Search for: All records

Not AvailableActor systems are a flexible model of concurrent and distributed programming, which are efficiently implementable, and avoid many classic concurrency bugs by construction. However they must still deal with the challenge of messages arriving in unexpected orders. We describe an approach to restricting the orders in which actors send messages to each other, by equipping actor references—the handle used to address another actor—with a protocol restricting which message types can be sent to another actor and in which order using that particular actor reference. This endows the actor references with the properties of (flow-sensitive) static capabilities, which we call actor capabilities. By sending other actors only restricted actor references, actors may control which messages are sent in which orders by other actors. Rules for duplicating (splitting) actor references ensure that these restrictions apply even in the presence of delegation. The capabilities themselves restrict message send ordering, which may form the foundation for stronger forms of reasoning. We demonstrate this by layering an effect system over the base type system, where the relationships enforced between the actor capabilities and the effects of an actor’s behaviour ensure that an actor’s behaviour is always prepared to handle any message that may arrive. 

Although they differ in the functionality they offer, low-level systems exhibit certain patterns of design and utilization of computing resources. In this paper we examine how modalities have emerged as a common structure in formal verification of low-level software, and explain how many recent examples naturally share common structure in the relationship between the modalities and software features they are used to reason about. We explain how the concept of a resource context (a class of system resources to reason about) naturally corresponds to families of modal operators indexed by system data, and how this naturally leads to using modal assertions to describe resource elements (data in the relevant context). 

Virtual memory management (VMM) code is a critical piece of general-purpose OS kernels, but verification of this functionality is challenging due to the complexity of the hardware interface (the page tables are updated via writes to those memory locations, using addresses which are themselves virtualized). Prior work on verification of VMM code has either only handled a single address space, or trusted significant pieces of assembly code. In this paper, we introduce a modal abstraction to describe the truth of assertions relative to a specific virtual address space: [r]P indicating that P holds in the virtual address space rooted at r. Such modal assertions allow different address spaces to refer to each other, enabling complete verification of instruction sequences manipulating multiple address spaces. Using them effectively requires working with other assertions, such as points-to assertions about memory contents — which implicitly depend on the address space they are used in. We therefore define virtual points-to assertions to definitionally mimic hardware address translation, relative to a page table root. We demonstrate our approach with challenging fragments of VMM code showing that our approach handles examples beyond what prior work can address, including reasoning about a sequence of instructions as it changes address spaces. Our results are formalized for a RISC-like fragment of x86-64 assembly in Rocq. 

Research in programming languages and software engineering are broadly concerned with the study of aspects of computer programs: their syntactic structure, the relationship between form and meaning (semantics), empirical properties of how they are constructed and deployed, and more. We could equally well apply this description to the range of ways in which linguistics studies the form, meaning, and use of natural language. We argue that despite some notable examples of PL and SE research drawing on ideas from natural language processing, there are still a wealth of concepts, techniques, and conceptual framings originating in linguistics which would be of use to PL and SE research. Moreover we show that beyond mere parallels, there are cases where linguistics research has complementary methodologies, may help explain or predict study outcomes, or offer new perspectives on established research areas in PL and SE. Broadly, we argue that researchers across PL and SE are investigating close cousins of problems actively studied for years by linguists, and familiarity with linguistics research seems likely to bear fruit for many PL and SE researchers. 

Temporal logics cover important classes of system specifications dealing with system behavior over time. Despite the prevalence of long-running systems that accept repeated input and output, and thus the clear relevance of temporal specifications to training software engineers, temporal logics are rarely taught to undergraduates. We motivate and describe an approach to teaching temporal specifications and temporal reasoning indirectly through teaching students about mocking dependencies, which is widely used in software testing of large systems (and therefore of more obvious relevance to students), less notationally intimidating to students, and still teaches similar reasoning principles. We report on 7 years of experience using this indirect approach to behavioral specifications in a software quality course. 

We describe a new concrete approach to giving predictable error locations for sequential (flow-sensitive) effect systems. Prior implementations of sequential effect systems rely on either computing a bottom-up effect and comparing it to a declaration (e.g., method annotation) or leaning on constraint-based type inference. These approaches do not necessarily report program locations that precisely indicate where a program may “go wrong” at runtime. Instead of relying on constraint solving, we draw on the notion of a residual from literature on ordered algebraic structures. Applying these to effect quantales (a large class of sequential effect systems) yields an implementation approach which accepts exactly the same program as an original effect quantale, but for effect-incorrect programs is guaranteed to fail type-checking with predictable error locations tied to evaluation order. We have implemented this idea in a generic effect system implementation framework for Java, and report on experiences applying effect systems from the literature and novel effect systems to Java programs. We find that the reported error locations with our technique are significantly closer to the program points that lead to failed effect checks. 

Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may have been mistranslated from a claim made in natural language. This is especially problematic when using proof assistants to formally verify the correctness of software with respect to a natural language specification. The translation from informal to formal remains a challenging, time-consuming process that is difficult to audit for correctness. This paper shows that it is possible to build support for specifications written in expressive subsets of natural language, within existing proof assistants, consistent with the principles used to establish trust and auditability in proof assistants themselves. We implement a means to provide specifications in a modularly extensible formal subset of English, and have them automatically translated into formal claims, entirely within the Lean proof assistant. Our approach is extensible (placing no permanent restrictions on grammatical structure), modular (allowing information about new words to be distributed alongside libraries), and produces proof certificates explaining how each word was interpreted and how the sentence's structure was used to compute the meaning. We apply our prototype to the translation of various English descriptions of formal specifications from a popular textbook into Lean formalizations; all can be translated correctly with a modest lexicon with only minor modifications related to lexicon size. 

Abstract Scyphomedusae are widespread in the oceans and their swimming has provided valuable insights into the hydrodynamics of animal propulsion. Most of this research has focused on symmetrical, linear swimming. However, in nature, medusae typically swim circuitous, nonlinear paths involving frequent turns. Here we describe swimming turns by the scyphomedusaAurelia auritaduring which asymmetric bell margin motions produce rotation around a linearly translating body center. These jellyfish ‘skid’ through turns and the degree of asynchrony between opposite bell margins is an approximate predictor of turn magnitude during a pulsation cycle. The underlying neuromechanical organization of bell contraction contributes substantially to asynchronous bell motions and inserts a stochastic rotational component into the directionality of scyphomedusan swimming. These mechanics are important for natural populations because asynchronous bell contraction patterns are commonin situand result in frequent turns by naturally swimming medusae. 

Peptide nucleic acids (PNAs) are high-affinity synthetic nucleic acid analogs capable of hybridization with native nucleic acids. PNAs synthesized having amino acid sidechains installed at the γ-position along the backbone provide a template for a single biopolymer to simultaneously encode nucleic acid and amino acid sequences. Previously, we reported the development of “bilingual” PNAs through the synthesis of an amphiphilic sequence featuring separate blocks of hydrophobic and hydrophilic amino acid functional groups. These PNAs combined the sequence-specific binding activity of nucleic acids with the structural organization properties of peptides. Like other amphiphilic compounds, these γ-PNAs were observed to assemble spontaneously into micelle-like nanostructures in aqueous solutions and disassembly was induced through hybridization to a complementary sequence. Here, we explore whether assembly of these bilingual PNAs is possible by harnessing the nucleic acid code. Specifically, we designed an amphiphile-masking duplex system in which spontaneous amphiphile assembly is prevented through hybridization to a nucleic acid masking sequence. We show that the amphiphile is displaced upon introduction of a releasing sequence complementary to the masking sequence through toehold mediated displacement. Upon release, we observe that the amphiphile proceeds to assemble in a fashion consistent with our previously reported structures. Our approach represents a novel method for controlled stimuli-responsive assembly of PNA-based nanostructures.